;; Copyright (c) 2015 Microsoft Corporation

(set-logic QF_FP)
(set-info :source "Handcrafted by CM Wintersteiger")
(set-info :status unsat)

(define-sort FPN () (_ FloatingPoint 11 53))
(declare-const x FPN)
(declare-const y FPN)
(declare-const r FPN)

(push)
(assert (= x (_ +zero 11 53)))
(assert (= y (_ +zero 11 53)))
(assert (= r (fp.rem x y)))
(assert (not (= r (_ NaN 11 53))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (_ +zero 11 53)))
(assert (= y (fp #b0 #b01111111111 #x0000000000000)))
(assert (= r (fp.rem x y)))
(assert (not (= r (_ +zero 11 53))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (_ -zero 11 53)))
(assert (= y (fp #b0 #b01111111111 #x0000000000000)))
(assert (= r (fp.rem x y)))
(assert (not (= r (_ -zero 11 53))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b10000000001 #xC000000000000)))
(assert (= y (fp #b0 #b10000000001 #x0000000000000)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b1 #b01111111111 #x0000000000000)))) 
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b01111111110 #xAAAAAAAAAAAAA)))
(assert (= y (fp #b0 #b10000000000 #x0000000000000)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b0 #b01111111110 #xAAAAAAAAAAAAA)))) 
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b00000000000 #x8000000000000)))
(assert (= y (fp #b0 #b00000000000 #x4000000000000)))
(assert (= r (fp.rem x y)))
(assert (not (= r (_ +zero 11 53))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b00000000000 #x0000000000002)))
(assert (= y (fp #b0 #b00000000000 #x0000000000001)))
(assert (= r (fp.rem x y)))
(assert (not (= r (_ +zero 11 53))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b00000000001 #x0000000000002)))
(assert (= y (fp #b0 #b00000000001 #x0000000000001)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b0 #b00000000000 #x0000000000001))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b10000000100 #x8000000000001)))
(assert (= y (fp #b0 #b01111111111 #x0800000000001)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b1 #b01111111101 #xE00000000003C))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b10000000000 #x0000000000000)))
(assert (= y (fp #b0 #b01111111111 #x8000000000000)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b0 #b01111111110 #x0000000000000))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b1 #b10011111101 #xA87E25EDC4BB5)))
(assert (= y (fp #b1 #b10011110011 #xE8364DDB1FEA2)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b1 #b10011110010 #x579A168BF2998))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b1 #b11010101100 #xBA496DA6FD793)))
(assert (= y (fp #b0 #b11010101000 #x5E71D0D8BC926)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b1 #b11010100110 #x0ECA2604708E0))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b1 #b11001110011 #x4C72393703C65)))
(assert (= y (fp #b1 #b11001100111 #xD6CABF4562BD9)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b1 #b11001100110 #x525558C9DF128))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b01001010001 #x7A1E15D14E5BF)))
(assert (= y      (fp #b1 #b01001001000 #x7527CE0F3ED04)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b1 #b01001000110 #x1E1C792E81470))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b10000110100 #x0000000000000)))
(assert (= y (fp #b1 #b01111111111 #x0000000000000)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b0 #b00000000000 #x0000000000000))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b00101110100 #xC7A45FFD68A0B)))
(assert (= y (fp #b1 #b00101110101 #x97CF87669C19A)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b1 #b00101110100 #x67FAAECFCF929))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b00000000000 #x0000000000001)))
(assert (= y (fp #b1 #b00000000000 #x0000000000002)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b0 #b00000000000 #x0000000000001))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b00000000000 #x6D94D95948562)))
(assert (= y (fp #b0 #b00000000000 #xCDED95B5422BF)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b1 #b00000000000 #x6058BC5BF9D5D))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(push)
(assert (= x (fp #b0 #b01101000100 #xE821F8D041F88)))
(assert (= y (fp #b0 #b01101100010 #xA4731A475E745)))
(assert (= r (fp.rem x y)))
(assert (not (= r (fp #b0 #b01101000100 #xE821F8D041F88))))
(check-sat-using qffp)
;; (check-sat-using (then fpa2bv smt))
(pop)

(exit)
